ds:x:Id fp Type, da:a:Knd fp Type, init:x:Id fp ds(x)?Void,
pre:a:Id fp State(ds)Valtype(da;locl(a))Prop,
ef:kx:KndId fp State(ds)Valtype(da;1of(kx))ds(2of(kx))?Void,
send:kl:KndIdLnk fp
send:(tg:Id(State(ds)Valtype(da;1of(kl))(da(rcv(2of(kl),tg))?Void List))) List,
frame:x:Id fp Knd List, sframe:ltg:IdLnkId fp Knd List, aframe:k:Knd fp Id List,
bframe:k:Knd fp IdLnk List, rframe:x:Id fp Knd List.
mk-ma(ds;
da;
init;
pre;
ef;
send;
frame;
sframe;
aframe;
bframe;
rframe)
 MsgA 

latex

Definitions	Void, t  T, x:A. B(x), Top, Id, Knd, type List, x. t(x), x:A. B(x), a:A fp B(a), x:AB(x), IdLnk, Type, x.A(x), 2of(t), rcv(l,tg), KindDeq, f(x)?z, 1of(t), Valtype(da;k), x:AB(x), State(ds), IdDeq, Prop, locl(a), Unit, , <a,b>, mk-ma, MsgA, #$n, a<b, False, P  Q, A, AB, , {x:A| B(x) }, , Atom, left+right
Lemmas	it wf, locl wf, id-deq wf, ma-state wf, ma-valtype wf, pi1 wf, fpf-cap wf, Kind-deq wf, rcv wf, pi2 wf, IdLnk wf, fpf wf, Knd wf, Id wf, top wf